\begin{tabbing}
$\forall$$T$:Type, $P$:(($T$ List)$\rightarrow$Prop).
\\[0ex]($\forall$$L$:$T$ List. Dec($P$($L$)))
\\[0ex]$\Rightarrow$ (\=$\forall$$L$:$T$ List.\+
\\[0ex]$P$($L$) $\Rightarrow$ ($\exists$${\it L'}$:$T$ List. ${\it L'}$ $\leq$ $L$ \& $P$(${\it L'}$) \& ($\forall$${\it L''}$:$T$ List. ${\it L''}$ $\leq$ ${\it L'}$ $\Rightarrow$ $P$(${\it L''}$) $\Rightarrow$ ${\it L''}$ $=$ ${\it L'}$)))
\-
\end{tabbing}